\begin{tabbing}
$\forall$${\it es}$:event\_system\{i:l\}, $l$:IdLnk, ${\it tg}$:Id, $e$:es{-}E(${\it es}$).
\\[0ex](es{-}kind(${\it es}$; $e$) = rcv($l$,${\it tg}$) $\in$ Knd)
\\[0ex]$\Rightarrow$ guard(\=(($\uparrow$es{-}isrcv(${\it es}$; $e$))\+
\\[0ex]c$\wedge$ \=((es{-}lnk(${\it es}$; $e$) = $l$)\+
\\[0ex]$\wedge$ (es{-}tag(${\it es}$; $e$) = ${\it tg}$)
\\[0ex]$\wedge$ (loc(es{-}sender(${\it es}$; $e$)) = source($l$) $\in$ Id))))
\-\-
\end{tabbing}